#include "locks.h"
#include <stdio.h>

#define TRUE 1
#define FALSE 0


// Bank Account Example

// Account structure
typedef struct {
  int balance;
  KSPIN_LOCK lock;
} ACCOUNT, *PACCOUNT;


PACCOUNT create(int b) {
  PACCOUNT acc = (PACCOUNT) malloc(sizeof(ACCOUNT));
  acc->balance = b;
  InitializeSpinLock(&acc->lock);
  return acc;
}

int read(PACCOUNT acc) {
  return acc->balance;
}

void deposit(PACCOUNT acc, int n) {
  AcquireSpinLock(&acc->lock);
  acc->balance = acc->balance + n;
  ReleaseSpinLock(&acc->lock);
}

//#define BUG1
//#define BUG2

void withdraw(PACCOUNT acc, int n, int* withdrawn) {
  int r;
#ifdef BUG1 //double lock acquire
  AcquireSpinLock(&acc->lock);
#endif

#ifndef BUG2
  AcquireSpinLock(&acc->lock);
#endif
  r = read(acc);
  if (r >= n) {
#ifdef BUG2 //atomicity violation
    AcquireSpinLock(&acc->lock);
#endif
    acc->balance = r - n;
    ReleaseSpinLock(&acc->lock);
    *withdrawn = TRUE;
    return;
  }
  *withdrawn = FALSE;
}


// Harness

// Thread 1
void deposit_test(PACCOUNT acc, int n) {
  deposit(acc, n);
}

// Thread 2
void withdraw_test(PACCOUNT acc, int n, int* withdrawn) {
  withdraw(acc, n, withdrawn);
}

// #define CONCRETE
// #define SEQUENTIAL

void storm_main() {
  PACCOUNT acc;
  int withdrawn;
  int x, y, z;

  // Initialization
  withdrawn = FALSE;
#ifdef CONCRETE
  x = 10;
  y = 5;
  z = 10;
#else
  x = storm_nondet();
  y = storm_nondet();
  z = storm_nondet();
#endif
  acc = create(x);

  // Threads
#ifdef SEQUENTIAL
  deposit_test(acc, y); // deposit
  withdraw_test(acc, z, &withdrawn); // withdraw
#else
  __async_call deposit_test(acc, y); // deposit
  __async_call withdraw_test(acc, z, &withdrawn); // withdraw
#endif

  STORM_END; // Join
  STORM_ASSERT(!withdrawn || read(acc) == x + y - z);
}

void main() {}

